(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x4 () (_ BitVec 32))
(declare-fun x5 () (_ BitVec 32))
(assert (let ((?v_16 (bvsub x1 (_ bv30 32))) (?v_17 (bvadd x3 x4))) (let ((?v_13 (bvadd (_ bv0 32) x2))) (let ((?v_15 (bvadd ?v_13 x0))) (let ((?v_20 (bvadd ?v_15 (_ bv0 32))) (?v_8 (bvadd x0 (_ bv2 32)))) (let ( (?v_2 (bvsub (_ bv56 32) ?v_8))) (and true (bvult ?v_16 (bvadd (bvadd x5 ?v_17) (_ bv24 32))) true (bvult ?v_2 (_ bv63 32)) true (bvule x2 x0) true (bvule x0 ?v_15) (= (_ bv38 32) x4) true (= (_ bv104 32) x5) true (= ?v_20 x3) true (bvult (_ bv480 32) x1) true)))))))
(check-sat)
(exit)
